\newcommand{\sadt}{\mbox{\sc Sadt}}
\newcommand{\spectre}{\mbox{\sc Spectre}}
\newcommand{\cifre}{\mbox{\sc Cifre}}
\newcommand{\spin}{\mbox{\sc Spin-N4}}
\newcommand{\coo}{\mbox{\sc CO3-N4}}
\newcommand{\esterel}{\mbox{\sc Esterel}}
\newcommand{\lustre}{\mbox{\sc Lustre}}
\newcommand{\appliuf}{\mbox{APPLIUF5}}
\newcommand{\pollux}{\mbox{\sc Pollux}}
\newcommand{\perle}{\mbox{\sc Perle}}
\newcommand{\pam}{\mbox{\sc Pam}}
\newcommand{\pab}{\mbox{\sc Pab}}
\newcommand{\lca}{\mbox{\sc Lca}}
\newcommand{\refi}{\mbox{$\downarrow$}}
%\newcommand{\p}[1]{\mbox{${\cal P}(#1)$}}
\newcommand{\e}[1]{\mbox{${\cal E}(#1)$}}
\newcommand{\p}{\mbox{${\cal P}$}}
\newcommand{\s}{\mbox{${\cal S}$}}
%\newcommand{\e}{\mbox{${\cal E}$}}
\newcommand{\lucid}{\mbox{\sc Lucid}}
\newcommand{\cesar}{\mbox{\sc Cesar}}
\newcommand{\xesar}{\mbox{\sc Xesar}}
\newcommand{\lesar}{\mbox{\sc Lesar}}
\newcommand{\lurette}{\mbox{\sc Lurette}}
\newcommand{\lutin}{\mbox{\sc Lutin}}
\newcommand{\polka}{\mbox{{\sc Polka}}}
\newcommand{\argos}{\mbox{\sc Argos}}
\newcommand{\sahara}{\mbox{\sc Sahara}}
\newcommand{\statecharts}{\mbox{\sc Statecharts}}
\newcommand{\sml}{\mbox{\sc Sml}}
\newcommand{\auto}{\mbox{\sc Auto}}
\newcommand{\autograph}{\mbox{\sc Autograph}}
\newcommand{\lustrevdeux}{\mbox{\sc Lustre-V2}}
\newcommand{\lustrevtrois}{\mbox{\sc Lustre-V3}}
\newcommand{\signal}{\mbox{\sc Signal}}
\newcommand{\saga}{\mbox{\sc Saga}}
\newcommand{\oc}{\mbox{\sc oc}}
\newcommand{\ic}{\mbox{\sc ic}}
\newcommand{\aldebaran}{\mbox{\sc Aldebaran}}
\newcommand{\prog}[1]{\mbox{\tt #1}}
\newcommand{\fby}{\mbox{\tt ->}}
\newcommand{\sprog}[1]{\mbox{\scriptsize\tt #1}}
\newcommand{\Vrai}{{\it vrai\/}}
\newcommand{\Faux}{{\it faux\/}}
\newcommand{\true}{\mbox{\it true\/}}
\newcommand{\false}{\mbox{\it false\/}}
%\newcommand{\TT}{\mbox{\it tt\/}}
%\newcommand{\FF}{\mbox{\it ff\/}}
\newcommand{\nil}{\mbox{\it nil\/}}
\newcommand{\lfp}{\mbox{\it lfp\/}}
\newcommand{\since}{{\cal S}}
\newcommand{\suite}[2]{(#1_0,\ldots,#1_{#2})}
\newcommand{\seq}[1]{(#1_0,\ldots,#1_n,\ldots)}
\newcommand{\pre}{\bullet}
\newcommand{\wpre}{\underline{\pre}}
\newcommand{\Pre}{\mbox{\it pre\/}}
\newcommand{\sat}[1]{\models_{#1}}
\newcommand{\implies}{{\scriptstyle \supset}}
\newcommand{\until}{\:{\cal U}\:}
%\newcommand{\next}{{\bigcirc}}
\newcommand{\suchthat}{\mbox{ such that }}
\newcommand{\trans}[1]{\mbox{$\stackrel{#1}{\longrightarrow}$}}
\newcommand{\Trans}[1]{\mbox{$\stackrel{#1}{\rightarrow}$}}
\newcommand{\power}{\mbox{\^{}}}
\newcommand{\transrel}[2]{
    \mbox{$ {\displaystyle \mbox{  }
                 \frac{\raisebox{-0.4ex}[1.1ex][0in]
                              {$\scriptstyle #1$}
                      }
                      {\raisebox{0.6ex}[0in][0.3ex]
                                {$\scriptstyle #2$}
                      } 
             }\!\!\!\!\rightarrow $} }
\newcommand{\transrell}[1]{
    \;\;
    \frac{\;\;#1}{\quad}\!\!\!\!\rightarrow
}
\newcommand{\rel}[1]{\stackrel{#1}{\rightarrow}}
\newcommand{\Mon}{{\it Mon\/}}
\newcommand{\ZZ}{\mbox{$\,\mbox{{\sf Z}}\!\!\!\!\!\mbox{{\sf Z}}\,\,$}}
\newcommand{\QQ}{\mbox{$\;$\makebox[0pt]{\raisebox{2pt}{$\scriptscriptstyle \mid\mid\;\,$}}$\!\!\!$\sf Q}}
\newcommand{\CC}{\mbox{l\hspace{-.47em}C}}
\newcommand{\NN}{\mbox{$\mathrm{I}\!\mathrm{N}$}}
\newcommand{\BB}{\mbox{\rm$\mbox{I}\!\mbox{B}$}}
\newcommand{\bool}{\mbox{$\mbox{I}\!\mbox{B}$}}
\newcommand{\RR}{\mbox{$\mbox{I}\!\mbox{R}$}}
\newcommand{\MGM}{{\sc mgm}}
\renewcommand{\iff}{\mbox{ $\;$iff$\;$ }}
\newcommand{\myand}{\mbox{ and }}
\newcommand{\rhobar}{{\overline{\rho}}}
\newcommand{\pibar}{{\overline{\pi}}}
\newcommand{\post}[1]{\mbox{\it post}_{#1}}
\newcommand{\Post}{\mbox{\it post\/}}
\newcommand{\pretilde}{\stackrel{\sim}{\mbox{\it pre}}}
\newcommand{\split}{\mbox{\it split\/}}
\newcommand{\err}{\mbox{\it err\/}}
\newcommand{\sem}[1]{[\![#1]\!]}

\renewcommand{\o}[1]{$\overline{\tt #1}$}
\renewcommand{\b}[1]{\,\overline{#1}\,}
\newcommand{\bb}[1]{$\,\overline{\mbox{#1}}\,$}
\renewcommand{\v}[1]{\,\vec{#1}\,}



\newcommand{\para}{\vspace{0.3cm} \par \noindent}
\newcommand{\Item}{\vspace{-2mm}\item[-]}
\newcommand{\cdeuxa}{C$^2$A}
\newcommand{\ctx}[1]{\makebox[0pt]{\rm #1}}
\newcommand{\ltx}[1]{\makebox[0pt][l]{\rm #1}}
\newcommand{\rtx}[1]{\makebox[0pt][r]{\rm #1}}
\newcommand{\cty}[1]{\makebox[0pt]{\tt #1}}
\newcommand{\rty}[1]{\makebox[0pt][r]{\tt #1}}
\newcommand{\lty}[1]{\makebox[0pt][l]{\tt #1}}
\newcommand{\cmth}[1]{\makebox[0pt]{$#1$}}
\newcommand{\lmth}[1]{\makebox[0pt][l]{$#1$}}
\newcommand{\rmth}[1]{\makebox[0pt][r]{$#1$}}
\newcommand{\ccbox}[2]{\parbox{#1}{\centering #2}}
\newcommand{\rbox}[2]{\parbox{#1}{\begin{flushright}#2\end{flushright}}}
\newcommand{\pretild}{\mbox{$\widetilde{\Pre}$}}
\newcommand{\et}{\;\wedge\;}
\newcommand{\mathspace}[1]{\rule[-#1]{0pt}{#1}}

\newlength{\magic}
\setlength{\magic}{28.35cm}
\newcommand{\postscript}[2]
    {\par\vspace{1ex}%\begin{center}
       \mbox{\psfig{rheight=#1,rwidth=12cm,bbllx=3.1714cm,bblly=0cm,bburx=0cm,bbury=13cm,figure=#2.ps}}%test1
       %\mbox{\psfig{rheight=#1,rwidth=14cm,bbllx=0cm,bblly=0cm,bburx=21cm,bbury=29.7cm,figure=#2.ps}}%test1
       %\mbox{\psfig{rheight=#1,rwidth=14cm,bbllx=3.1714cm,bblly=0cm,bburx=0cm,bbury=\magic,figure=#2.ps}}%test
     %\end{center}
	\vspace{1ex}\par}


\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}
\newtheorem{lemme}{Lemme}
\newtheorem{corollary}{Corollary}
\newtheorem{Definition}{Definition}
\newtheorem{Theoreme}{Th\'{e}or\`{e}me}
\newenvironment{proof}{\noindent{\it Proof:}}{{\Large $\Box$}}
\newenvironment{preuve}{{\it D\'emonstration:}}{{\Large $\Box$}}
\newenvironment{Exemple}{{\it Exemple:}}{\noindent{\it Fin de l'exemple.}}
\newenvironment{Example}{\paragraph{Example:}}{\noindent{\it [End of example]}}

\newenvironment{program}{\tt\vspace{0.0cm}\par \begin{minipage}{\fboxrule}\begin{tabbing} XX \= XX  \= XX  \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= \+\kill}{\end{tabbing} \end{minipage}\vspace{0.0cm}\rm\noindent\par}

\newenvironment{smallprogram}{\vspace{0.3cm}\par \begin{minipage}{\fboxrule}\small\tt\begin{tabbing} XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= XX \= \+\kill}{\end{tabbing} \end{minipage}\vspace{0.3cm}\rm\noindent\par}

\newenvironment{syntax}{~\\\begin{tabular*}{\textwidth}[t]{rcl}}{\end{tabular*}\vspace{0.3cm}}

\newcommand{\indexentry}[2]{\item #1  #2}
\newcommand{\subindexentry}[2]{\item {--- #1}  #2}
%\newcommand{\CC}{\mbox{\tt >}}
%\newcommand{\OO}{\mbox{\tt <}}


\newcommand{\equival}{\mbox{$\Leftrightarrow$}}
\newcommand{\implique}{\mbox{$\Rightarrow$}}

\newcommand{\Bool}{\mbox{{\rm I}$\!${\rm B}}}

%\newcommand{\Rule}[2]{\[ \mbox{$#1$} \over \mbox{$#2$} \]}
%\newcommand{\Rule}[2]{\mbox{$ \mbox{$#1$} \over \mbox{$#2$} $}}
\newcommand{\Rule}[2]{\mbox{$\displaystyle \frac{#1}{#2}$}}

%%%% GUILLEMETS
\newcommand{\og}{\raise0.27ex\hbox{$\scriptscriptstyle\ll$}\,}
\newcommand{\fg}{\raise0.27ex\hbox{\,$\scriptscriptstyle\gg$}}

%insertion de figure latex
\newcommand{\figinput}[3]{\begin{figure}[htbp]
            \begin{center}
            \input{#1}
            \caption{\mbox{#2}}
            \label{#3}
            \end{center}
           \end{figure}}

%insertion de figure ps
\newcommand{\psScaleInput}[4]{\begin{figure}[htbp]
   \begin{center}
   \scalebox{#1}{ \includegraphics{#2.ps}}
   \caption{#3}
   \label{#4}
   \end{center}
\end{figure}}

%insertion d'image
\newcommand{\imageinput}[4]{\begin{figure}[htbp]
   \begin{center}
   \scalebox{#1}{ \includegraphics{#2}}
   \caption{#3}
   \label{#4}
   \end{center}
\end{figure}}

% MINI BDD
\newcommand{\bintree}[3]{
\mbox{
        \raisebox{-.2in}{
                \setlength{\unitlength}{0.0125in}%
                \begin{picture}(35,44)(0,0)
                \thicklines
                \put( 20,30){\line( 1,-2){  7.600}}
                \put( 15,30){\line(-1,-2){  7.600}}
                \put( 33,12){\makebox(0,0)[t]{\mbox{#3}}}
                \put( 3,12){\makebox(0,0)[t]{\mbox{#2}}}
                \put( 15,34){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\mbox{#1}}}}
                \end{picture}
        }
}
}

\newcommand{\Bintree}[3]{
\mbox{
        \raisebox{-.2in}{
                \setlength{\unitlength}{0.0125in}%
                \begin{picture}(69,44)(-17,0)
                \thicklines
                \put( 20,30){\line(3,-2){19.500}}
                \put( 15,30){\line(-3,-2){19.500}}
                \put( 44,15){\makebox(0,0)[t]{\mbox{#3}}}
                \put( -8,15){\makebox(0,0)[t]{\mbox{#2}}}
                \put( 15,34){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\mbox{#1}}}}
                \end{picture}
        }
}
}
\newcommand{\rectree}[3]{
\mbox{
         \raisebox{-.05in}{
                \rule[-0.40in]{0in}{0.9in}
                \setlength{\unitlength}{0.0125in}%
                \begin{picture}(69,44)(-17,0)
                \thicklines
                \put( 20,30){\line(3,-2){19.500}}
                \put( 15,30){\line(-3,-2){19.500}}
                \put( 44,15){\makebox(0,0)[t]{\mbox{#3}}}
                \put( -8,15){\makebox(0,0)[t]{\mbox{#2}}}
                \put( 15,34){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\mbox{#1}}}}
                \end{picture}   
          }
}
}
\newcommand{\BINtree}[3]{
\mbox{
         \raisebox{-.05in}{
                \rule[-0.40in]{0in}{0.9in}
                \setlength{\unitlength}{0.0125in}%
                \begin{picture}(69,44)(-17,0)
                \thicklines
                \put( 20,30){\line(3,-2){19.500}}
                \put( 15,30){\line(-3,-2){19.500}}
                \put( 44,15){\makebox(0,0)[lt]{\mbox{#3}}}
                \put( -8,15){\makebox(0,0)[rt]{\mbox{#2}}}
                \put( 15,34){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\mbox{#1}}}}
                \end{picture}   
          }
}
}
\newcommand{\Rectree}[3]{ 
\mbox{   
         \raisebox{0.15in}{
                \rule[-0.80in]{0.0in}{1.3in}
                \setlength{\unitlength}{0.0125in}%
                \begin{picture}(69,44)(-17,0)
                \thicklines
                \put( 20,30){\line(3,-2){19.500}}
                \put( 15,30){\line(-3,-2){19.500}}
                \put( 44,15){\makebox(0,0)[t]{\mbox{#3}}}
                \put( -8,15){\makebox(0,0)[t]{\mbox{#2}}}
                \put( 15,34){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\mbox{#1}}}}
                \end{picture}
          }
}
}

\newcommand{\RECtree}[3]{ 
\mbox{   
         \raisebox{0.15in}{
                \rule[-0.80in]{0.0in}{1.3in}
                \setlength{\unitlength}{0.0125in}%
                %\begin{picture}(69,44)(-17,0)
                \begin{picture}(140,44)(-51,0)
                \thicklines
                \put( 20,30){\line(3,-1){34.00}}
                \put( 15,30){\line(-3,-1){34.00}}
                \put( 66,15){\makebox(0,0)[t]{\mbox{#3}}}
                \put( -32,15){\makebox(0,0)[t]{\mbox{#2}}}
                \put( 15,34){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\mbox{#1}}}}
                \end{picture}
          }
}
}
